CPAchecker Report

Find only exact matches

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

	Rank	Scope
-V-		{{line.bestrank}}		{{line.desc}}

Precondition (initial variable assignment):

{{fault.rank}}.

Details:

Current values:

Name	Value

{{sourceFiles[selectedSourceFile]}}

// Automatically generated by cegarmc  
//  
  
extern void __VERIFIER_assume(int);  
extern int __VERIFIER_nondet_bool();  
extern char __VERIFIER_nondet_char();  
extern signed char __VERIFIER_nondet_schar();  
extern unsigned char __VERIFIER_nondet_uchar();  
extern int __VERIFIER_nondet_int();  
extern unsigned int __VERIFIER_nondet_uint();  
extern short __VERIFIER_nondet_short();  
extern unsigned short __VERIFIER_nondet_ushort();  
extern long __VERIFIER_nondet_long();  
extern unsigned long __VERIFIER_nondet_ulong();  
extern long long __VERIFIER_nondet_longlong();  
extern unsigned long long __VERIFIER_nondet_ull();  
extern float __VERIFIER_nondet_float();  
extern double __VERIFIER_nondet_double();  
extern long double __VERIFIER_nondet_longdouble();  
extern void * __VERIFIER_nondet_pointer();  
  
int D_print_i;  
int D_print_st;  
int D_z;  
int N_generate_i;  
int N_generate_st;  
int S1_addsub_i;  
int S1_addsub_st;  
int S2_presdbl_i;  
int S2_presdbl_st;  
int S3_zero_i;  
int S3_zero_st;  
int count;  
int main_clk_ev;  
int main_clk_neg_edge;  
int main_clk_pos_edge;  
int main_clk_req_up;  
int main_clk_val;  
int main_clk_val_t;  
int main_dbl_ev;  
int main_dbl_req_up;  
int main_dbl_val;  
int main_dbl_val_t;  
int main_diff_ev;  
int main_diff_req_up;  
int main_diff_val;  
int main_diff_val_t;  
int main_in1_ev;  
int main_in1_req_up;  
int main_in1_val;  
int main_in1_val_t;  
int main_in2_ev;  
int main_in2_req_up;  
int main_in2_val;  
int main_in2_val_t;  
int main_pres_ev;  
int main_pres_req_up;  
int main_pres_val;  
int main_pres_val_t;  
int main_sum_ev;  
int main_sum_req_up;  
int main_sum_val;  
int main_sum_val_t;  
int main_zero_ev;  
int main_zero_req_up;  
int main_zero_val;  
int main_zero_val_t;  
int res;  
  
void error();  
void N_generate();  
void S1_addsub();  
void S2_presdbl();  
void S3_zero();  
void D_print();  
void eval();  
void start_simulation();  
  
  
void error() {  
  {  
  goto ERROR;  
  ERROR: ;  
  return;  
  }  
}  
  
void N_generate() {  
  auto int a;  
  auto int b;  
  {  
    main_in1_val_t = __VERIFIER_nondet_int();  
  main_in1_req_up = 1;  
    main_in2_val_t = __VERIFIER_nondet_int();  
  main_in2_req_up = 1;  
  return;  
  }  
}  
  
void S1_addsub() {  
  auto int a;  
  auto int b;  
  {  
  a = main_in1_val;  
  b = main_in2_val;  
  main_sum_val_t = a + b;  
  main_sum_req_up = 1;  
  main_diff_val_t = a - b;  
  main_diff_req_up = 1;  
  return;  
  }  
}  
  
void S2_presdbl() {  
  auto int a;  
  auto int b;  
  auto int c;  
  auto int d;  
  {  
  a = main_sum_val;  
  b = main_diff_val;  
  main_pres_val_t = a;  
  main_pres_req_up = 1;  
  c = a + b;  
  d = a - b;  
  main_dbl_val_t = c + d;  
  main_dbl_req_up = 1;  
  return;  
  }  
}  
  
void S3_zero() {  
  auto int a;  
  auto int b;  
  {  
  a = main_pres_val;  
  b = main_dbl_val;  
  main_zero_val_t = b - (a + a);  
  main_zero_req_up = 1;  
  return;  
  }  
}  
  
void D_print() {  
  {  
  D_z = main_zero_val;  
  return;  
  }  
}  
  
void eval() {  
  auto int tmp;  
  auto int tmp___0;  
  auto int tmp___1;  
  auto int tmp___2;  
  auto int tmp___3;  
  {  
  {  
    while (1) {  
      {  
        while_0_continue: ;  
        if (N_generate_st == 0) {  
          }  
        else {  
          if (S1_addsub_st == 0) {  
            }  
          else {  
            if (S2_presdbl_st == 0) {  
              }  
            else {  
              if (S3_zero_st == 0) {  
                }  
              else {  
                if (D_print_st == 0) {  
                  }  
                else {  
                  goto while_0_break;  
                  }  
                }  
              }  
            }  
          }  
        if (N_generate_st == 0) {  
          {  
                        tmp = __VERIFIER_nondet_int();  
            }  
          if (tmp) {  
            N_generate_st = 1;  
                        N_generate();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        if (S1_addsub_st == 0) {  
          {  
                        tmp___0 = __VERIFIER_nondet_int();  
            }  
          if (tmp___0) {  
            S1_addsub_st = 1;  
                        S1_addsub();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        if (S2_presdbl_st == 0) {  
          {  
                        tmp___1 = __VERIFIER_nondet_int();  
            }  
          if (tmp___1) {  
            S2_presdbl_st = 1;  
                        S2_presdbl();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        if (S3_zero_st == 0) {  
          {  
                        tmp___2 = __VERIFIER_nondet_int();  
            }  
          if (tmp___2) {  
            S3_zero_st = 1;  
                        S3_zero();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        if (D_print_st == 0) {  
          {  
                        tmp___3 = __VERIFIER_nondet_int();  
            }  
          if (tmp___3) {  
            D_print_st = 1;  
                        D_print();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        }  
      }  
    while_0_break: ;  
    }  
  return;  
  }  
}  
  
void start_simulation() {  
  auto int kernel_st;  
  {  
  kernel_st = 0;  
  if (main_in1_req_up == 1) {  
    if (main_in1_val != main_in1_val_t) {  
      main_in1_val = main_in1_val_t;  
      main_in1_ev = 0;  
      }  
    else {  
      }  
    main_in1_req_up = 0;  
    }  
  else {  
    }  
  if (main_in2_req_up == 1) {  
    if (main_in2_val != main_in2_val_t) {  
      main_in2_val = main_in2_val_t;  
      main_in2_ev = 0;  
      }  
    else {  
      }  
    main_in2_req_up = 0;  
    }  
  else {  
    }  
  if (main_sum_req_up == 1) {  
    if (main_sum_val != main_sum_val_t) {  
      main_sum_val = main_sum_val_t;  
      main_sum_ev = 0;  
      }  
    else {  
      }  
    main_sum_req_up = 0;  
    }  
  else {  
    }  
  if (main_diff_req_up == 1) {  
    if (main_diff_val != main_diff_val_t) {  
      main_diff_val = main_diff_val_t;  
      main_diff_ev = 0;  
      }  
    else {  
      }  
    main_diff_req_up = 0;  
    }  
  else {  
    }  
  if (main_pres_req_up == 1) {  
    if (main_pres_val != main_pres_val_t) {  
      main_pres_val = main_pres_val_t;  
      main_pres_ev = 0;  
      }  
    else {  
      }  
    main_pres_req_up = 0;  
    }  
  else {  
    }  
  if (main_dbl_req_up == 1) {  
    if (main_dbl_val != main_dbl_val_t) {  
      main_dbl_val = main_dbl_val_t;  
      main_dbl_ev = 0;  
      }  
    else {  
      }  
    main_dbl_req_up = 0;  
    }  
  else {  
    }  
  if (main_zero_req_up == 1) {  
    if (main_zero_val != main_zero_val_t) {  
      main_zero_val = main_zero_val_t;  
      main_zero_ev = 0;  
      }  
    else {  
      }  
    main_zero_req_up = 0;  
    }  
  else {  
    }  
  if (main_clk_req_up == 1) {  
    if (main_clk_val != main_clk_val_t) {  
      main_clk_val = main_clk_val_t;  
      main_clk_ev = 0;  
      if (main_clk_val == 1) {  
        main_clk_pos_edge = 0;  
        main_clk_neg_edge = 2;  
        }  
      else {  
        main_clk_neg_edge = 0;  
        main_clk_pos_edge = 2;  
        }  
      }  
    else {  
      }  
    main_clk_req_up = 0;  
    }  
  else {  
    }  
  if (N_generate_i == 1) {  
    N_generate_st = 0;  
    }  
  else {  
    N_generate_st = 2;  
    }  
  if (S1_addsub_i == 1) {  
    S1_addsub_st = 0;  
    }  
  else {  
    S1_addsub_st = 2;  
    }  
  if (S2_presdbl_i == 1) {  
    S2_presdbl_st = 0;  
    }  
  else {  
    S2_presdbl_st = 2;  
    }  
  if (S3_zero_i == 1) {  
    S3_zero_st = 0;  
    }  
  else {  
    S3_zero_st = 2;  
    }  
  if (D_print_i == 1) {  
    D_print_st = 0;  
    }  
  else {  
    D_print_st = 2;  
    }  
  if (main_in1_ev == 0) {  
    main_in1_ev = 1;  
    }  
  else {  
    }  
  if (main_in2_ev == 0) {  
    main_in2_ev = 1;  
    }  
  else {  
    }  
  if (main_sum_ev == 0) {  
    main_sum_ev = 1;  
    }  
  else {  
    }  
  if (main_diff_ev == 0) {  
    main_diff_ev = 1;  
    }  
  else {  
    }  
  if (main_pres_ev == 0) {  
    main_pres_ev = 1;  
    }  
  else {  
    }  
  if (main_dbl_ev == 0) {  
    main_dbl_ev = 1;  
    }  
  else {  
    }  
  if (main_zero_ev == 0) {  
    main_zero_ev = 1;  
    }  
  else {  
    }  
  if (main_clk_ev == 0) {  
    main_clk_ev = 1;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 0) {  
    main_clk_pos_edge = 1;  
    }  
  else {  
    }  
  if (main_clk_neg_edge == 0) {  
    main_clk_neg_edge = 1;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    N_generate_st = 0;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    S1_addsub_st = 0;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    S2_presdbl_st = 0;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    S3_zero_st = 0;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    D_print_st = 0;  
    }  
  else {  
    }  
  if (main_in1_ev == 1) {  
    main_in1_ev = 2;  
    }  
  else {  
    }  
  if (main_in2_ev == 1) {  
    main_in2_ev = 2;  
    }  
  else {  
    }  
  if (main_sum_ev == 1) {  
    main_sum_ev = 2;  
    }  
  else {  
    }  
  if (main_diff_ev == 1) {  
    main_diff_ev = 2;  
    }  
  else {  
    }  
  if (main_pres_ev == 1) {  
    main_pres_ev = 2;  
    }  
  else {  
    }  
  if (main_dbl_ev == 1) {  
    main_dbl_ev = 2;  
    }  
  else {  
    }  
  if (main_zero_ev == 1) {  
    main_zero_ev = 2;  
    }  
  else {  
    }  
  if (main_clk_ev == 1) {  
    main_clk_ev = 2;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    main_clk_pos_edge = 2;  
    }  
  else {  
    }  
  if (main_clk_neg_edge == 1) {  
    main_clk_neg_edge = 2;  
    }  
  else {  
    }  
  {  
    while (1) {  
      {  
        while_1_continue: ;  
        {  
          kernel_st = 1;  
                    eval();  
          }  
        kernel_st = 2;  
        if (main_in1_req_up == 1) {  
          if (main_in1_val != main_in1_val_t) {  
            main_in1_val = main_in1_val_t;  
            main_in1_ev = 0;  
            }  
          else {  
            }  
          main_in1_req_up = 0;  
          }  
        else {  
          }  
        if (main_in2_req_up == 1) {  
          if (main_in2_val != main_in2_val_t) {  
            main_in2_val = main_in2_val_t;  
            main_in2_ev = 0;  
            }  
          else {  
            }  
          main_in2_req_up = 0;  
          }  
        else {  
          }  
        if (main_sum_req_up == 1) {  
          if (main_sum_val != main_sum_val_t) {  
            main_sum_val = main_sum_val_t;  
            main_sum_ev = 0;  
            }  
          else {  
            }  
          main_sum_req_up = 0;  
          }  
        else {  
          }  
        if (main_diff_req_up == 1) {  
          if (main_diff_val != main_diff_val_t) {  
            main_diff_val = main_diff_val_t;  
            main_diff_ev = 0;  
            }  
          else {  
            }  
          main_diff_req_up = 0;  
          }  
        else {  
          }  
        if (main_pres_req_up == 1) {  
          if (main_pres_val != main_pres_val_t) {  
            main_pres_val = main_pres_val_t;  
            main_pres_ev = 0;  
            }  
          else {  
            }  
          main_pres_req_up = 0;  
          }  
        else {  
          }  
        if (main_dbl_req_up == 1) {  
          if (main_dbl_val != main_dbl_val_t) {  
            main_dbl_val = main_dbl_val_t;  
            main_dbl_ev = 0;  
            }  
          else {  
            }  
          main_dbl_req_up = 0;  
          }  
        else {  
          }  
        if (main_zero_req_up == 1) {  
          if (main_zero_val != main_zero_val_t) {  
            main_zero_val = main_zero_val_t;  
            main_zero_ev = 0;  
            }  
          else {  
            }  
          main_zero_req_up = 0;  
          }  
        else {  
          }  
        if (main_clk_req_up == 1) {  
          if (main_clk_val != main_clk_val_t) {  
            main_clk_val = main_clk_val_t;  
            main_clk_ev = 0;  
            if (main_clk_val == 1) {  
              main_clk_pos_edge = 0;  
              main_clk_neg_edge = 2;  
              }  
            else {  
              main_clk_neg_edge = 0;  
              main_clk_pos_edge = 2;  
              }  
            }  
          else {  
            }  
          main_clk_req_up = 0;  
          }  
        else {  
          }  
        kernel_st = 3;  
        if (main_in1_ev == 0) {  
          main_in1_ev = 1;  
          }  
        else {  
          }  
        if (main_in2_ev == 0) {  
          main_in2_ev = 1;  
          }  
        else {  
          }  
        if (main_sum_ev == 0) {  
          main_sum_ev = 1;  
          }  
        else {  
          }  
        if (main_diff_ev == 0) {  
          main_diff_ev = 1;  
          }  
        else {  
          }  
        if (main_pres_ev == 0) {  
          main_pres_ev = 1;  
          }  
        else {  
          }  
        if (main_dbl_ev == 0) {  
          main_dbl_ev = 1;  
          }  
        else {  
          }  
        if (main_zero_ev == 0) {  
          main_zero_ev = 1;  
          }  
        else {  
          }  
        if (main_clk_ev == 0) {  
          main_clk_ev = 1;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 0) {  
          main_clk_pos_edge = 1;  
          }  
        else {  
          }  
        if (main_clk_neg_edge == 0) {  
          main_clk_neg_edge = 1;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          N_generate_st = 0;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          S1_addsub_st = 0;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          S2_presdbl_st = 0;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          S3_zero_st = 0;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          D_print_st = 0;  
          }  
        else {  
          }  
        if (main_in1_ev == 1) {  
          main_in1_ev = 2;  
          }  
        else {  
          }  
        if (main_in2_ev == 1) {  
          main_in2_ev = 2;  
          }  
        else {  
          }  
        if (main_sum_ev == 1) {  
          main_sum_ev = 2;  
          }  
        else {  
          }  
        if (main_diff_ev == 1) {  
          main_diff_ev = 2;  
          }  
        else {  
          }  
        if (main_pres_ev == 1) {  
          main_pres_ev = 2;  
          }  
        else {  
          }  
        if (main_dbl_ev == 1) {  
          main_dbl_ev = 2;  
          }  
        else {  
          }  
        if (main_zero_ev == 1) {  
          main_zero_ev = 2;  
          }  
        else {  
          }  
        if (main_clk_ev == 1) {  
          main_clk_ev = 2;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          main_clk_pos_edge = 2;  
          }  
        else {  
          }  
        if (main_clk_neg_edge == 1) {  
          main_clk_neg_edge = 2;  
          }  
        else {  
          }  
        if (N_generate_st == 0) {  
          }  
        else {  
          if (S1_addsub_st == 0) {  
            }  
          else {  
            if (S2_presdbl_st == 0) {  
              }  
            else {  
              if (S3_zero_st == 0) {  
                }  
              else {  
                if (D_print_st == 0) {  
                  }  
                else {  
                  goto while_1_break;  
                  }  
                }  
              }  
            }  
          }  
        }  
      }  
    while_1_break: ;  
    }  
  return;  
  }  
}  
  
void main () {  
//  
// Number of lvals: 62  
//   Frama_C_interval: int (int min, int max)  
//      int (int min, int max)  
//   error: void (void)  
//      void (void)  
//   count: int  
//      int  
//   res: int  
//      int  
//   main_in1_val: int  
//      int  
//   main_in1_val_t: int  
//      int  
//   main_in1_ev: int  
//      int  
//   main_in1_req_up: int  
//      int  
//   main_in2_val: int  
//      int  
//   main_in2_val_t: int  
//      int  
//   main_in2_ev: int  
//      int  
//   main_in2_req_up: int  
//      int  
//   main_diff_val: int  
//      int  
//   main_diff_val_t: int  
//      int  
//   main_diff_ev: int  
//      int  
//   main_diff_req_up: int  
//      int  
//   main_sum_val: int  
//      int  
//   main_sum_val_t: int  
//      int  
//   main_sum_ev: int  
//      int  
//   main_sum_req_up: int  
//      int  
//   main_pres_val: int  
//      int  
//   main_pres_val_t: int  
//      int  
//   main_pres_ev: int  
//      int  
//   main_pres_req_up: int  
//      int  
//   main_dbl_val: int  
//      int  
//   main_dbl_val_t: int  
//      int  
//   main_dbl_ev: int  
//      int  
//   main_dbl_req_up: int  
//      int  
//   main_zero_val: int  
//      int  
//   main_zero_val_t: int  
//      int  
//   main_zero_ev: int  
//      int  
//   main_zero_req_up: int  
//      int  
//   main_clk_val: int  
//      int  
//   main_clk_val_t: int  
//      int  
//   main_clk_ev: int  
//      int  
//   main_clk_req_up: int  
//      int  
//   main_clk_pos_edge: int  
//      int  
//   main_clk_neg_edge: int  
//      int  
//   N_generate_st: int  
//      int  
//   N_generate_i: int  
//      int  
//   S1_addsub_st: int  
//      int  
//   S1_addsub_i: int  
//      int  
//   S2_presdbl_st: int  
//      int  
//   S2_presdbl_i: int  
//      int  
//   S3_zero_st: int  
//      int  
//   S3_zero_i: int  
//      int  
//   D_z: int  
//      int  
//   D_print_st: int  
//      int  
//   D_print_i: int  
//      int  
//   N_generate: void (void)  
//      void (void)  
//   S1_addsub: void (void)  
//      void (void)  
//   S2_presdbl: void (void)  
//      void (void)  
//   S3_zero: void (void)  
//      void (void)  
//   D_print: void (void)  
//      void (void)  
//   eval: void (void)  
//      void (void)  
//   start_simulation: void (void)  
//      void (void)  
//   n1: int  
//      int  
//   n2: int  
//      int  
//   n3: int  
//      int  
//   bound: int  
//      int  
//   i: int  
//      int  
//   flag: int  
//      int  
//  
  
D_print_i = __VERIFIER_nondet_int();  
D_print_st = __VERIFIER_nondet_int();  
D_z = __VERIFIER_nondet_int();  
N_generate_i = __VERIFIER_nondet_int();  
N_generate_st = __VERIFIER_nondet_int();  
S1_addsub_i = __VERIFIER_nondet_int();  
S1_addsub_st = __VERIFIER_nondet_int();  
S2_presdbl_i = __VERIFIER_nondet_int();  
S2_presdbl_st = __VERIFIER_nondet_int();  
S3_zero_i = __VERIFIER_nondet_int();  
S3_zero_st = __VERIFIER_nondet_int();  
count = __VERIFIER_nondet_int();  
main_clk_ev = __VERIFIER_nondet_int();  
main_clk_neg_edge = __VERIFIER_nondet_int();  
main_clk_pos_edge = __VERIFIER_nondet_int();  
main_clk_req_up = __VERIFIER_nondet_int();  
main_clk_val = __VERIFIER_nondet_int();  
main_clk_val_t = __VERIFIER_nondet_int();  
main_dbl_ev = __VERIFIER_nondet_int();  
main_dbl_req_up = __VERIFIER_nondet_int();  
main_dbl_val = __VERIFIER_nondet_int();  
main_dbl_val_t = __VERIFIER_nondet_int();  
main_diff_ev = __VERIFIER_nondet_int();  
main_diff_req_up = __VERIFIER_nondet_int();  
main_diff_val = __VERIFIER_nondet_int();  
main_diff_val_t = __VERIFIER_nondet_int();  
main_in1_ev = __VERIFIER_nondet_int();  
main_in1_req_up = __VERIFIER_nondet_int();  
main_in1_val = __VERIFIER_nondet_int();  
main_in1_val_t = __VERIFIER_nondet_int();  
main_in2_ev = __VERIFIER_nondet_int();  
main_in2_req_up = __VERIFIER_nondet_int();  
main_in2_val = __VERIFIER_nondet_int();  
main_in2_val_t = __VERIFIER_nondet_int();  
main_pres_ev = __VERIFIER_nondet_int();  
main_pres_req_up = __VERIFIER_nondet_int();  
main_pres_val = __VERIFIER_nondet_int();  
main_pres_val_t = __VERIFIER_nondet_int();  
main_sum_ev = __VERIFIER_nondet_int();  
main_sum_req_up = __VERIFIER_nondet_int();  
main_sum_val = __VERIFIER_nondet_int();  
main_sum_val_t = __VERIFIER_nondet_int();  
main_zero_ev = __VERIFIER_nondet_int();  
main_zero_req_up = __VERIFIER_nondet_int();  
main_zero_val = __VERIFIER_nondet_int();  
main_zero_val_t = __VERIFIER_nondet_int();  
res = __VERIFIER_nondet_int();  
  
  
  
{  
  int n1 = 3;  
  int n2 = 5;  
  int n3 = 7;  
  res = 0;  
  auto int bound;  
  bound = __VERIFIER_nondet_int();  
  __VERIFIER_assume(bound >= 1);  
  {  
    {  
      count = 0;  
      main_in1_ev = 2;  
      main_in1_req_up = 0;  
      main_in2_ev = 2;  
      main_in2_req_up = 0;  
      main_diff_ev = 2;  
      main_diff_req_up = 0;  
      main_sum_ev = 2;  
      main_sum_req_up = 0;  
      main_pres_ev = 2;  
      main_pres_req_up = 0;  
      main_dbl_ev = 2;  
      main_dbl_req_up = 0;  
      main_zero_ev = 2;  
      main_zero_req_up = 0;  
      main_clk_val = 0;  
      main_clk_ev = 2;  
      main_clk_req_up = 0;  
      main_clk_pos_edge = 2;  
      main_clk_neg_edge = 2;  
      count = 0;  
      N_generate_i = 0;  
      S1_addsub_i = 0;  
      S2_presdbl_i = 0;  
      S3_zero_i = 0;  
      D_print_i = 0;  
            start_simulation();  
      }  
    {  
      int i = 0;  
      while (1) {  
        if (i < bound) {  
          }  
        else {  
          break;  
          }  
        {  
          if (i % n1 == 0) {  
            if (i % n2 == 0) {  
              if (i % n3 == 0) {  
                res = i;  
                }  
              else {  
                }  
              }  
            else {  
              }  
            }  
          else {  
            }  
          i ++;  
          int flag = res;  
          while_2_continue: ;  
          {  
            main_clk_val_t = 1;  
            main_clk_req_up = 1;  
                        start_simulation();  
            count ++;  
            }  
  
	  if (res % 105 == 0) {  
	    ;  
	  } else {  
	    error();  
	  }  
	    
          if (count == 5) {  
            if (! (D_z == 0)) {  
              error();  
              }  
            else {  
              }  
            count = 0;  
            }  
          else {  
            }  
          {  
            main_clk_val_t = 0;  
            main_clk_req_up = 1;  
                        start_simulation();  
              
          }  
        }  
      }  
    }  
  }  
return;  
}}  

DateTimeLevelComponentMessage
2023-06-2804:16:58:978INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2023-06-2804:16:58:996INFOResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2023-06-2804:16:59:051INFOCPAchecker.runCPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started
2023-06-2804:16:59:071INFOCPAchecker.parseParsing CFA from file(s) "no_context/combo1.c"
2023-06-2804:17:00:114INFOCoreComponentsFactory.createAlgorithmUsing heuristics to select analysis
2023-06-2804:17:00:125WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
 cpa.callstack.unsupportedFunctions
 termination.violation.witness
 cpa.predicate.memoryAllocationsAlwaysSucceed
 cpa.arg.compressWitness
 cpa.callstack.skipFunctionPointerRecursion
 cpa.composite.aggregateBasicBlocks
 counterexample.export.graphml
 counterexample.export.compressWitness
 cpa.arg.proofWitness 
2023-06-2804:17:00:126INFOCPAchecker.runAlgorithmStarting analysis ...
2023-06-2804:17:00:130INFOSelectionAlgorithm.chooseConfigPerforming heuristic ...
2023-06-2804:17:00:135INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
ResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2023-06-2804:17:00:149INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
CoreComponentsFactory.createAlgorithmUsing Restarting Algorithm
2023-06-2804:17:00:155INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runLoading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ...
2023-06-2804:17:00:160INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-2804:17:00:161INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'.
2023-06-2804:17:00:161INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'.
2023-06-2804:17:00:163INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties
ResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 140s
2023-06-2804:17:00:464INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runStarting analysis 1 ...
2023-06-2804:19:07:182WARNINGAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
ShutdownNotifier.shutdownIfNecessaryWarning: Analysis 1 stopped. (The CPU-time limit of 140s has elapsed.)
2023-06-2804:19:07:372INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runRestartAlgorithm switches to the next configuration...
2023-06-2804:19:07:372INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runLoading analysis 2 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ...
2023-06-2804:19:07:375INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-2804:19:07:375INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu' has two values '900s' and '60s'. Using '60s'.
2023-06-2804:19:07:376INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu::required' has two values '900' and '60s'. Using '60s'.
2023-06-2804:19:07:376INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties
ResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 60s
2023-06-2804:19:07:429INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runStarting analysis 2 ...
2023-06-2804:19:07:522INFOCPAchecker.runAlgorithmStopping analysis ...

        

Date	Time	Level	Component	Message
2023-06-28	04:16:58:978	INFO	CPAMain.detectFrontendLanguageIfNecessary	Language C detected and set for analysis
2023-06-28	04:16:58:996	INFO	ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 900s
2023-06-28	04:16:59:051	INFO	CPAchecker.run	CPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started
2023-06-28	04:16:59:071	INFO	CPAchecker.parse	Parsing CFA from file(s) "no_context/combo1.c"
2023-06-28	04:17:00:114	INFO	CoreComponentsFactory.createAlgorithm	Using heuristics to select analysis
2023-06-28	04:17:00:125	WARNING	CPAchecker.printConfigurationWarnings	The following configuration options were specified but are not used: cpa.callstack.unsupportedFunctions termination.violation.witness cpa.predicate.memoryAllocationsAlwaysSucceed cpa.arg.compressWitness cpa.callstack.skipFunctionPointerRecursion cpa.composite.aggregateBasicBlocks counterexample.export.graphml counterexample.export.compressWitness cpa.arg.proofWitness
2023-06-28	04:17:00:126	INFO	CPAchecker.runAlgorithm	Starting analysis ...
2023-06-28	04:17:00:130	INFO	SelectionAlgorithm.chooseConfig	Performing heuristic ...
2023-06-28	04:17:00:135	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 900s
2023-06-28	04:17:00:149	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties CoreComponentsFactory.createAlgorithm	Using Restarting Algorithm
2023-06-28	04:17:00:155	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	Loading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ...
2023-06-28	04:17:00:160	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-28	04:17:00:161	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'.
2023-06-28	04:17:00:161	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'.
2023-06-28	04:17:00:163	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 140s
2023-06-28	04:17:00:464	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	Starting analysis 1 ...
2023-06-28	04:19:07:182	WARNING	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties ShutdownNotifier.shutdownIfNecessary	Warning: Analysis 1 stopped. (The CPU-time limit of 140s has elapsed.)
2023-06-28	04:19:07:372	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	RestartAlgorithm switches to the next configuration...
2023-06-28	04:19:07:372	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	Loading analysis 2 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ...
2023-06-28	04:19:07:375	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-28	04:19:07:375	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu' has two values '900s' and '60s'. Using '60s'.
2023-06-28	04:19:07:376	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu::required' has two values '900' and '60s'. Using '60s'.
2023-06-28	04:19:07:376	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 60s
2023-06-28	04:19:07:429	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	Starting analysis 2 ...
2023-06-28	04:19:07:522	INFO	CPAchecker.runAlgorithm	Stopping analysis ...

Statistics NameStatistics ValueAdditional Value
Selection Algorithm statistics
Size of preliminary analysis reached set      0
Used algorithm property                       /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Program containing only relevant bools        0
Relevant boolean vars / relevant vars ratio   0.0685
Requires alias handling                       0
Requires loop handling                        1
Has a single loop                             0
Requires composite-type handling              0
Requires array handling                       0
Requires float handling                       0
Requires recursion handling                   0
Relevant addressed vars / relevant vars ratio 0.0000
Program containing external functions         true
Number of all righthand side functions        9
Restart Algorithm statistics
Number of algorithms provided    7
Number of algorithms used        2
Total time for algorithm 2     0.150s
ValueAnalysisCPA statistics
Number of variables per state                     0.00 sum: 0, count: 1449, min: 0, max: 0
Number of global variables per state              0.00 sum: 0, count: 1449, min: 0, max: 0
Number of assumptions                                  670
Number of deterministic assumptions                      0
Level of Determinism                              0%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations                    1782
Total time for liveness abstraction                   0.000s
Total time for abstraction computation                0.004s
Total time for path thresholds                        0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA     0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (SVCOMP) statistics
Number of states                                  1
Total time for successor computation                  0.000s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 2120, count: 2120, min: 1, max: 1 [1 x 2120]
Number of states with assumption transitions      0
CPA algorithm statistics
Number of iterations            1449
Max size of waitlist            22
Average size of waitlist        12
Number of computed successors   1782
Max successors for one state    2
Number of times merged          0
Number of times stopped         334
Number of times breaked         0
Total time for CPA algorithm         0.082s Max:     0.082s
	  Time for choose from waitlist      0.017s
	  Time for precision adjustment      0.011s
	  Time for transfer relation         0.024s
	  Time for stop operator             0.003s
	  Time for adding to reached set     0.023s
ValueAnalysisRefiner statistics
Number of refinements                                    0
Number of targets found                                  0 count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement                        0.000s
Number of root relocations                               0
Number of similar, repeated refinements                  0
Number of unique precision increments             0
PathExtractor statistics
Total number of targets found            0
ValueAnalysisPathInterpolator statistics
	  Time for interpolation                              0.000s
	  Number of interpolations                               0
	  Number of interpolation queries                        0 count: 0, min: 0, max: 0, avg: 0.00
	  Size of interpolant                             0.00 sum: 0, count: 0, min: 0, max: 0
	  Number of sliced prefixes                              0 count: 0, min: 0, max: 0, avg: 0.00
	  Extracting infeasible sliced prefixes               0.000s
	  Selecting infeasible sliced prefixes                0.000s
CEGAR algorithm statistics
Number of CEGAR refinements          0
Counterexample-Check Algorithm statistics
Number of counterexample checks    0
CPA algorithm statistics
Number of iterations            1449
Max size of waitlist            22
Average size of waitlist        12
Number of computed successors   1782
Max successors for one state    2
Number of times merged          0
Number of times stopped         334
Number of times breaked         0
Total time for CPA algorithm         0.082s Max:     0.082s
	  Time for choose from waitlist      0.017s
	  Time for precision adjustment      0.011s
	  Time for transfer relation         0.024s
	  Time for stop operator             0.003s
	  Time for adding to reached set     0.023s
ValueAnalysisRefiner statistics
Number of refinements                                    0
Number of targets found                                  0 count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement                        0.000s
Number of root relocations                               0
Number of similar, repeated refinements                  0
Number of unique precision increments             0
PathExtractor statistics
Total number of targets found            0
ValueAnalysisPathInterpolator statistics
	  Time for interpolation                              0.000s
	  Number of interpolations                               0
	  Number of interpolation queries                        0 count: 0, min: 0, max: 0, avg: 0.00
	  Size of interpolant                             0.00 sum: 0, count: 0, min: 0, max: 0
	  Number of sliced prefixes                              0 count: 0, min: 0, max: 0, avg: 0.00
	  Extracting infeasible sliced prefixes               0.000s
	  Selecting infeasible sliced prefixes                0.000s
CEGAR algorithm statistics
Number of CEGAR refinements          0
Counterexample-Check Algorithm statistics
Number of counterexample checks    0
Code Coverage
	  Function coverage      1.000
	  Visited lines          455
	  Total lines            455
	  Line coverage          1.000
	  Visited conditions     234
	  Total conditions       234
	  Condition coverage     1.000
CPAchecker general statistics
Number of program locations                       732
Number of CFA edges (per node)                         861 count: 732, min: 0, max: 3, avg: 1.18
Number of relevant variables                      73
Number of functions                               9
Number of loops (and loop nodes)                         3 sum: 294, min: 40, max: 196, avg: 98.00
Size of reached set             1449
	  Number of reached locations   514 70%
		    Avg states per location     2
		    Max states per location     3 at node N7
	  Number of reached functions   9 100%
	  Number of target states       0
Time for analysis setup          1.055s
	  Time for loading CPAs          0.179s
	  Time for loading parser        0.156s
	  Time for CFA construction      0.693s
		    Time for parsing file(s)     0.262s
		    Time for AST to CFA          0.167s
		    Time for CFA sanity check    0.048s
		    Time for post-processing     0.152s
		    Time for CFA export          0.846s
			      Time for function pointers resolving            0.005s
				        Function calls via function pointers             0 count: 1, min: 0, max: 0, avg: 0.00
				        Instrumented function pointer calls              0 count: 1, min: 0, max: 0, avg: 0.00
				        Function calls with function pointer arguments        0 count: 1, min: 0, max: 0, avg: 0.00
				        Instrumented function pointer arguments          0 count: 1, min: 0, max: 0, avg: 0.00
			      Time for classifying variables                  0.090s
				        Time for collecting variables                 0.033s
				        Time for solving dependencies                 0.001s
				        Time for building hierarchy                   0.000s
				        Time for building classification              0.051s
				        Time for exporting data                       0.005s
Time for Analysis              127.396s
CPU time for analysis          141.440s
Time for analyzing result        0.001s
Total time for CPAchecker      128.452s
Total CPU time for CPAchecker  144.560s
Time for statistics              0.051s
Time for Garbage Collector       0.936s in 55 runs
Garbage Collector(s) used    G1 Old Generation, G1 Young Generation
Used heap memory                475MB (   453 MiB) max;    230MB (   219 MiB) avg;    481MB (   459 MiB) peak
Used non-heap memory             53MB (    50 MiB) max;     50MB (    48 MiB) avg;     53MB (    51 MiB) peak
Used in G1 Old Gen pool          94MB (    90 MiB) max;     61MB (    58 MiB) avg;     94MB (    90 MiB) peak
Allocated heap memory           638MB (   609 MiB) max;    544MB (   519 MiB) avg
Allocated non-heap memory        56MB (    53 MiB) max;     53MB (    51 MiB) avg
Total process virtual memory  12292MB ( 11723 MiB) max;  12284MB ( 11715 MiB) avg

        

Statistics Name	Statistics Value	Additional Value
Selection Algorithm statistics
Size of preliminary analysis reached set	0
Used algorithm property	/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Program containing only relevant bools	0
Relevant boolean vars / relevant vars ratio	0.0685
Requires alias handling	0
Requires loop handling	1
Has a single loop	0
Requires composite-type handling	0
Requires array handling	0
Requires float handling	0
Requires recursion handling	0
Relevant addressed vars / relevant vars ratio	0.0000
Program containing external functions	true
Number of all righthand side functions	9
Restart Algorithm statistics
Number of algorithms provided	7
Number of algorithms used	2
Total time for algorithm 2	0.150s
ValueAnalysisCPA statistics
Number of variables per state	0.00	sum: 0, count: 1449, min: 0, max: 0
Number of global variables per state	0.00	sum: 0, count: 1449, min: 0, max: 0
Number of assumptions	670
Number of deterministic assumptions	0
Level of Determinism	0%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations	1782
Total time for liveness abstraction	0.000s
Total time for abstraction computation	0.004s
Total time for path thresholds	0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA	0.000s
Replaced symbolic expressions	0
AutomatonAnalysis (SVCOMP) statistics
Number of states	1
Total time for successor computation	0.000s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 2120, count: 2120, min: 1, max: 1 [1 x 2120]
Number of states with assumption transitions	0
CPA algorithm statistics
Number of iterations	1449
Max size of waitlist	22
Average size of waitlist	12
Number of computed successors	1782
Max successors for one state	2
Number of times merged	0
Number of times stopped	334
Number of times breaked	0
Total time for CPA algorithm	0.082s	Max: 0.082s
Time for choose from waitlist	0.017s
Time for precision adjustment	0.011s
Time for transfer relation	0.024s
Time for stop operator	0.003s
Time for adding to reached set	0.023s
ValueAnalysisRefiner statistics
Number of refinements	0
Number of targets found	0	count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement	0.000s
Number of root relocations	0
Number of similar, repeated refinements	0
Number of unique precision increments	0
PathExtractor statistics
Total number of targets found	0
ValueAnalysisPathInterpolator statistics
Time for interpolation	0.000s
Number of interpolations	0
Number of interpolation queries	0	count: 0, min: 0, max: 0, avg: 0.00
Size of interpolant	0.00	sum: 0, count: 0, min: 0, max: 0
Number of sliced prefixes	0	count: 0, min: 0, max: 0, avg: 0.00
Extracting infeasible sliced prefixes	0.000s
Selecting infeasible sliced prefixes	0.000s
CEGAR algorithm statistics
Number of CEGAR refinements	0
Counterexample-Check Algorithm statistics
Number of counterexample checks	0
CPA algorithm statistics
Number of iterations	1449
Max size of waitlist	22
Average size of waitlist	12
Number of computed successors	1782
Max successors for one state	2
Number of times merged	0
Number of times stopped	334
Number of times breaked	0
Total time for CPA algorithm	0.082s	Max: 0.082s
Time for choose from waitlist	0.017s
Time for precision adjustment	0.011s
Time for transfer relation	0.024s
Time for stop operator	0.003s
Time for adding to reached set	0.023s
ValueAnalysisRefiner statistics
Number of refinements	0
Number of targets found	0	count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement	0.000s
Number of root relocations	0
Number of similar, repeated refinements	0
Number of unique precision increments	0
PathExtractor statistics
Total number of targets found	0
ValueAnalysisPathInterpolator statistics
Time for interpolation	0.000s
Number of interpolations	0
Number of interpolation queries	0	count: 0, min: 0, max: 0, avg: 0.00
Size of interpolant	0.00	sum: 0, count: 0, min: 0, max: 0
Number of sliced prefixes	0	count: 0, min: 0, max: 0, avg: 0.00
Extracting infeasible sliced prefixes	0.000s
Selecting infeasible sliced prefixes	0.000s
CEGAR algorithm statistics
Number of CEGAR refinements	0
Counterexample-Check Algorithm statistics
Number of counterexample checks	0
Code Coverage
Function coverage	1.000
Visited lines	455
Total lines	455
Line coverage	1.000
Visited conditions	234
Total conditions	234
Condition coverage	1.000
CPAchecker general statistics
Number of program locations	732
Number of CFA edges (per node)	861	count: 732, min: 0, max: 3, avg: 1.18
Number of relevant variables	73
Number of functions	9
Number of loops (and loop nodes)	3	sum: 294, min: 40, max: 196, avg: 98.00
Size of reached set	1449
Number of reached locations	514	70%
Avg states per location	2
Max states per location	3	at node N7
Number of reached functions	9	100%
Number of target states	0
Time for analysis setup	1.055s
Time for loading CPAs	0.179s
Time for loading parser	0.156s
Time for CFA construction	0.693s
Time for parsing file(s)	0.262s
Time for AST to CFA	0.167s
Time for CFA sanity check	0.048s
Time for post-processing	0.152s
Time for CFA export	0.846s
Time for function pointers resolving	0.005s
Function calls via function pointers	0	count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls	0	count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments	0	count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments	0	count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables	0.090s
Time for collecting variables	0.033s
Time for solving dependencies	0.001s
Time for building hierarchy	0.000s
Time for building classification	0.051s
Time for exporting data	0.005s
Time for Analysis	127.396s
CPU time for analysis	141.440s
Time for analyzing result	0.001s
Total time for CPAchecker	128.452s
Total CPU time for CPAchecker	144.560s
Time for statistics	0.051s
Time for Garbage Collector	0.936s	in 55 runs
Garbage Collector(s) used	G1 Old Generation, G1 Young Generation
Used heap memory	475MB ( 453 MiB) max; 230MB ( 219 MiB) avg; 481MB ( 459 MiB) peak
Used non-heap memory	53MB ( 50 MiB) max; 50MB ( 48 MiB) avg; 53MB ( 51 MiB) peak
Used in G1 Old Gen pool	94MB ( 90 MiB) max; 61MB ( 58 MiB) avg; 94MB ( 90 MiB) peak
Allocated heap memory	638MB ( 609 MiB) max; 544MB ( 519 MiB) avg
Allocated non-heap memory	56MB ( 53 MiB) max; 53MB ( 51 MiB) avg
Total process virtual memory	12292MB ( 11723 MiB) max; 12284MB ( 11715 MiB) avg

#Configuration NameConfiguration Value
1analysis.entryFunction  main
2analysis.name  svcomp23
3analysis.programNames  no_context/combo1.c
4analysis.selectAnalysisHeuristically  true
5analysis.summaryEdges  true
6cfa.simplifyCfa  false
7cfa.useCFACloningForMultiThreadedPrograms  true
8counterexample.export.compressWitness  false
9counterexample.export.graphml  witness.graphml
10cpa.arg.compressWitness  false
11cpa.arg.proofWitness  witness.graphml
12cpa.callstack.skipFunctionPointerRecursion  true
13cpa.callstack.unsupportedFunctions  pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow
14cpa.composite.aggregateBasicBlocks  false
15cpa.predicate.memoryAllocationsAlwaysSucceed  true
16datarace.config  svcomp23--datarace.properties
17heuristicSelection.addressedRatio  0.0
18heuristicSelection.complexLoopConfig  components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties
19heuristicSelection.loopConfig  components/svcomp23--multipleLoopsConfig.properties
20heuristicSelection.loopFreeConfig  components/svcomp23--configselection-restart-bmc-fallbacks.properties
21heuristicSelection.singleLoopConfig  components/svcomp23--singleLoopConfig.properties
22language  C
23limits.time.cpu  900s
24limits.time.cpu::required  900
25log.level  INFO
26memorycleanup.config  svcomp23--memorycleanup.properties
27memorysafety.config  svcomp23--memorysafety.properties
28overflow.config  svcomp23--overflow.properties
29parser.usePreprocessor  true
30specification  /home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp
31statistics.print  true
32termination.config  svcomp23--termination.properties
33termination.violation.witness  witness.graphml

        

#	Configuration Name	Configuration Value
1	analysis.entryFunction	main
2	analysis.name	svcomp23
3	analysis.programNames	no_context/combo1.c
4	analysis.selectAnalysisHeuristically	true
5	analysis.summaryEdges	true
6	cfa.simplifyCfa	false
7	cfa.useCFACloningForMultiThreadedPrograms	true
8	counterexample.export.compressWitness	false
9	counterexample.export.graphml	witness.graphml
10	cpa.arg.compressWitness	false
11	cpa.arg.proofWitness	witness.graphml
12	cpa.callstack.skipFunctionPointerRecursion	true
13	cpa.callstack.unsupportedFunctions	pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow
14	cpa.composite.aggregateBasicBlocks	false
15	cpa.predicate.memoryAllocationsAlwaysSucceed	true
16	datarace.config	svcomp23--datarace.properties
17	heuristicSelection.addressedRatio	0.0
18	heuristicSelection.complexLoopConfig	components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties
19	heuristicSelection.loopConfig	components/svcomp23--multipleLoopsConfig.properties
20	heuristicSelection.loopFreeConfig	components/svcomp23--configselection-restart-bmc-fallbacks.properties
21	heuristicSelection.singleLoopConfig	components/svcomp23--singleLoopConfig.properties
22	language	C
23	limits.time.cpu	900s
24	limits.time.cpu::required	900
25	log.level	INFO
26	memorycleanup.config	svcomp23--memorycleanup.properties
27	memorysafety.config	svcomp23--memorysafety.properties
28	overflow.config	svcomp23--overflow.properties
29	parser.usePreprocessor	true
30	specification	/home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp
31	statistics.print	true
32	termination.config	svcomp23--termination.properties
33	termination.violation.witness	witness.graphml

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

Source: {{dependency.repository}}

License:

Full text of license

{{dependencies.licenses[dependency.licenseId]}}

Report for no_context/combo1.c

About

{{dependency.name}} {{dependency.version}}

1	// Automatically generated by cegarmc
2	//
3
4	extern void __VERIFIER_assume(int);
5	extern int __VERIFIER_nondet_bool();
6	extern char __VERIFIER_nondet_char();
7	extern signed char __VERIFIER_nondet_schar();
8	extern unsigned char __VERIFIER_nondet_uchar();
9	extern int __VERIFIER_nondet_int();
10	extern unsigned int __VERIFIER_nondet_uint();
11	extern short __VERIFIER_nondet_short();
12	extern unsigned short __VERIFIER_nondet_ushort();
13	extern long __VERIFIER_nondet_long();
14	extern unsigned long __VERIFIER_nondet_ulong();
15	extern long long __VERIFIER_nondet_longlong();
16	extern unsigned long long __VERIFIER_nondet_ull();
17	extern float __VERIFIER_nondet_float();
18	extern double __VERIFIER_nondet_double();
19	extern long double __VERIFIER_nondet_longdouble();
20	extern void * __VERIFIER_nondet_pointer();
21
22	int D_print_i;
23	int D_print_st;
24	int D_z;
25	int N_generate_i;
26	int N_generate_st;
27	int S1_addsub_i;
28	int S1_addsub_st;
29	int S2_presdbl_i;
30	int S2_presdbl_st;
31	int S3_zero_i;
32	int S3_zero_st;
33	int count;
34	int main_clk_ev;
35	int main_clk_neg_edge;
36	int main_clk_pos_edge;
37	int main_clk_req_up;
38	int main_clk_val;
39	int main_clk_val_t;
40	int main_dbl_ev;
41	int main_dbl_req_up;
42	int main_dbl_val;
43	int main_dbl_val_t;
44	int main_diff_ev;
45	int main_diff_req_up;
46	int main_diff_val;
47	int main_diff_val_t;
48	int main_in1_ev;
49	int main_in1_req_up;
50	int main_in1_val;
51	int main_in1_val_t;
52	int main_in2_ev;
53	int main_in2_req_up;
54	int main_in2_val;
55	int main_in2_val_t;
56	int main_pres_ev;
57	int main_pres_req_up;
58	int main_pres_val;
59	int main_pres_val_t;
60	int main_sum_ev;
61	int main_sum_req_up;
62	int main_sum_val;
63	int main_sum_val_t;
64	int main_zero_ev;
65	int main_zero_req_up;
66	int main_zero_val;
67	int main_zero_val_t;
68	int res;
69
70	void error();
71	void N_generate();
72	void S1_addsub();
73	void S2_presdbl();
74	void S3_zero();
75	void D_print();
76	void eval();
77	void start_simulation();
78
79
80	void error() {
81	{
82	goto ERROR;
83	ERROR: ;
84	return;
85	}
86	}
87
88	void N_generate() {
89	auto int a;
90	auto int b;
91	{
92	main_in1_val_t = __VERIFIER_nondet_int();
93	main_in1_req_up = 1;
94	main_in2_val_t = __VERIFIER_nondet_int();
95	main_in2_req_up = 1;
96	return;
97	}
98	}
99
100	void S1_addsub() {
101	auto int a;
102	auto int b;
103	{
104	a = main_in1_val;
105	b = main_in2_val;
106	main_sum_val_t = a + b;
107	main_sum_req_up = 1;
108	main_diff_val_t = a - b;
109	main_diff_req_up = 1;
110	return;
111	}
112	}
113
114	void S2_presdbl() {
115	auto int a;
116	auto int b;
117	auto int c;
118	auto int d;
119	{
120	a = main_sum_val;
121	b = main_diff_val;
122	main_pres_val_t = a;
123	main_pres_req_up = 1;
124	c = a + b;
125	d = a - b;
126	main_dbl_val_t = c + d;
127	main_dbl_req_up = 1;
128	return;
129	}
130	}
131
132	void S3_zero() {
133	auto int a;
134	auto int b;
135	{
136	a = main_pres_val;
137	b = main_dbl_val;
138	main_zero_val_t = b - (a + a);
139	main_zero_req_up = 1;
140	return;
141	}
142	}
143
144	void D_print() {
145	{
146	D_z = main_zero_val;
147	return;
148	}
149	}
150
151	void eval() {
152	auto int tmp;
153	auto int tmp___0;
154	auto int tmp___1;
155	auto int tmp___2;
156	auto int tmp___3;
157	{
158	{
159	while (1) {
160	{
161	while_0_continue: ;
162	if (N_generate_st == 0) {
163	}
164	else {
165	if (S1_addsub_st == 0) {
166	}
167	else {
168	if (S2_presdbl_st == 0) {
169	}
170	else {
171	if (S3_zero_st == 0) {
172	}
173	else {
174	if (D_print_st == 0) {
175	}
176	else {
177	goto while_0_break;
178	}
179	}
180	}
181	}
182	}
183	if (N_generate_st == 0) {
184	{
185	tmp = __VERIFIER_nondet_int();
186	}
187	if (tmp) {
188	N_generate_st = 1;
189	N_generate();
190	}
191	else {
192	}
193	}
194	else {
195	}
196	if (S1_addsub_st == 0) {
197	{
198	tmp___0 = __VERIFIER_nondet_int();
199	}
200	if (tmp___0) {
201	S1_addsub_st = 1;
202	S1_addsub();
203	}
204	else {
205	}
206	}
207	else {
208	}
209	if (S2_presdbl_st == 0) {
210	{
211	tmp___1 = __VERIFIER_nondet_int();
212	}
213	if (tmp___1) {
214	S2_presdbl_st = 1;
215	S2_presdbl();
216	}
217	else {
218	}
219	}
220	else {
221	}
222	if (S3_zero_st == 0) {
223	{
224	tmp___2 = __VERIFIER_nondet_int();
225	}
226	if (tmp___2) {
227	S3_zero_st = 1;
228	S3_zero();
229	}
230	else {
231	}
232	}
233	else {
234	}
235	if (D_print_st == 0) {
236	{
237	tmp___3 = __VERIFIER_nondet_int();
238	}
239	if (tmp___3) {
240	D_print_st = 1;
241	D_print();
242	}
243	else {
244	}
245	}
246	else {
247	}
248	}
249	}
250	while_0_break: ;
251	}
252	return;
253	}
254	}
255
256	void start_simulation() {
257	auto int kernel_st;
258	{
259	kernel_st = 0;
260	if (main_in1_req_up == 1) {
261	if (main_in1_val != main_in1_val_t) {
262	main_in1_val = main_in1_val_t;
263	main_in1_ev = 0;
264	}
265	else {
266	}
267	main_in1_req_up = 0;
268	}
269	else {
270	}
271	if (main_in2_req_up == 1) {
272	if (main_in2_val != main_in2_val_t) {
273	main_in2_val = main_in2_val_t;
274	main_in2_ev = 0;
275	}
276	else {
277	}
278	main_in2_req_up = 0;
279	}
280	else {
281	}
282	if (main_sum_req_up == 1) {
283	if (main_sum_val != main_sum_val_t) {
284	main_sum_val = main_sum_val_t;
285	main_sum_ev = 0;
286	}
287	else {
288	}
289	main_sum_req_up = 0;
290	}
291	else {
292	}
293	if (main_diff_req_up == 1) {
294	if (main_diff_val != main_diff_val_t) {
295	main_diff_val = main_diff_val_t;
296	main_diff_ev = 0;
297	}
298	else {
299	}
300	main_diff_req_up = 0;
301	}
302	else {
303	}
304	if (main_pres_req_up == 1) {
305	if (main_pres_val != main_pres_val_t) {
306	main_pres_val = main_pres_val_t;
307	main_pres_ev = 0;
308	}
309	else {
310	}
311	main_pres_req_up = 0;
312	}
313	else {
314	}
315	if (main_dbl_req_up == 1) {
316	if (main_dbl_val != main_dbl_val_t) {
317	main_dbl_val = main_dbl_val_t;
318	main_dbl_ev = 0;
319	}
320	else {
321	}
322	main_dbl_req_up = 0;
323	}
324	else {
325	}
326	if (main_zero_req_up == 1) {
327	if (main_zero_val != main_zero_val_t) {
328	main_zero_val = main_zero_val_t;
329	main_zero_ev = 0;
330	}
331	else {
332	}
333	main_zero_req_up = 0;
334	}
335	else {
336	}
337	if (main_clk_req_up == 1) {
338	if (main_clk_val != main_clk_val_t) {
339	main_clk_val = main_clk_val_t;
340	main_clk_ev = 0;
341	if (main_clk_val == 1) {
342	main_clk_pos_edge = 0;
343	main_clk_neg_edge = 2;
344	}
345	else {
346	main_clk_neg_edge = 0;
347	main_clk_pos_edge = 2;
348	}
349	}
350	else {
351	}
352	main_clk_req_up = 0;
353	}
354	else {
355	}
356	if (N_generate_i == 1) {
357	N_generate_st = 0;
358	}
359	else {
360	N_generate_st = 2;
361	}
362	if (S1_addsub_i == 1) {
363	S1_addsub_st = 0;
364	}
365	else {
366	S1_addsub_st = 2;
367	}
368	if (S2_presdbl_i == 1) {
369	S2_presdbl_st = 0;
370	}
371	else {
372	S2_presdbl_st = 2;
373	}
374	if (S3_zero_i == 1) {
375	S3_zero_st = 0;
376	}
377	else {
378	S3_zero_st = 2;
379	}
380	if (D_print_i == 1) {
381	D_print_st = 0;
382	}
383	else {
384	D_print_st = 2;
385	}
386	if (main_in1_ev == 0) {
387	main_in1_ev = 1;
388	}
389	else {
390	}
391	if (main_in2_ev == 0) {
392	main_in2_ev = 1;
393	}
394	else {
395	}
396	if (main_sum_ev == 0) {
397	main_sum_ev = 1;
398	}
399	else {
400	}
401	if (main_diff_ev == 0) {
402	main_diff_ev = 1;
403	}
404	else {
405	}
406	if (main_pres_ev == 0) {
407	main_pres_ev = 1;
408	}
409	else {
410	}
411	if (main_dbl_ev == 0) {
412	main_dbl_ev = 1;
413	}
414	else {
415	}
416	if (main_zero_ev == 0) {
417	main_zero_ev = 1;
418	}
419	else {
420	}
421	if (main_clk_ev == 0) {
422	main_clk_ev = 1;
423	}
424	else {
425	}
426	if (main_clk_pos_edge == 0) {
427	main_clk_pos_edge = 1;
428	}
429	else {
430	}
431	if (main_clk_neg_edge == 0) {
432	main_clk_neg_edge = 1;
433	}
434	else {
435	}
436	if (main_clk_pos_edge == 1) {
437	N_generate_st = 0;
438	}
439	else {
440	}
441	if (main_clk_pos_edge == 1) {
442	S1_addsub_st = 0;
443	}
444	else {
445	}
446	if (main_clk_pos_edge == 1) {
447	S2_presdbl_st = 0;
448	}
449	else {
450	}
451	if (main_clk_pos_edge == 1) {
452	S3_zero_st = 0;
453	}
454	else {
455	}
456	if (main_clk_pos_edge == 1) {
457	D_print_st = 0;
458	}
459	else {
460	}
461	if (main_in1_ev == 1) {
462	main_in1_ev = 2;
463	}
464	else {
465	}
466	if (main_in2_ev == 1) {
467	main_in2_ev = 2;
468	}
469	else {
470	}
471	if (main_sum_ev == 1) {
472	main_sum_ev = 2;
473	}
474	else {
475	}
476	if (main_diff_ev == 1) {
477	main_diff_ev = 2;
478	}
479	else {
480	}
481	if (main_pres_ev == 1) {
482	main_pres_ev = 2;
483	}
484	else {
485	}
486	if (main_dbl_ev == 1) {
487	main_dbl_ev = 2;
488	}
489	else {
490	}
491	if (main_zero_ev == 1) {
492	main_zero_ev = 2;
493	}
494	else {
495	}
496	if (main_clk_ev == 1) {
497	main_clk_ev = 2;
498	}
499	else {
500	}
501	if (main_clk_pos_edge == 1) {
502	main_clk_pos_edge = 2;
503	}
504	else {
505	}
506	if (main_clk_neg_edge == 1) {
507	main_clk_neg_edge = 2;
508	}
509	else {
510	}
511	{
512	while (1) {
513	{
514	while_1_continue: ;
515	{
516	kernel_st = 1;
517	eval();
518	}
519	kernel_st = 2;
520	if (main_in1_req_up == 1) {
521	if (main_in1_val != main_in1_val_t) {
522	main_in1_val = main_in1_val_t;
523	main_in1_ev = 0;
524	}
525	else {
526	}
527	main_in1_req_up = 0;
528	}
529	else {
530	}
531	if (main_in2_req_up == 1) {
532	if (main_in2_val != main_in2_val_t) {
533	main_in2_val = main_in2_val_t;
534	main_in2_ev = 0;
535	}
536	else {
537	}
538	main_in2_req_up = 0;
539	}
540	else {
541	}
542	if (main_sum_req_up == 1) {
543	if (main_sum_val != main_sum_val_t) {
544	main_sum_val = main_sum_val_t;
545	main_sum_ev = 0;
546	}
547	else {
548	}
549	main_sum_req_up = 0;
550	}
551	else {
552	}
553	if (main_diff_req_up == 1) {
554	if (main_diff_val != main_diff_val_t) {
555	main_diff_val = main_diff_val_t;
556	main_diff_ev = 0;
557	}
558	else {
559	}
560	main_diff_req_up = 0;
561	}
562	else {
563	}
564	if (main_pres_req_up == 1) {
565	if (main_pres_val != main_pres_val_t) {
566	main_pres_val = main_pres_val_t;
567	main_pres_ev = 0;
568	}
569	else {
570	}
571	main_pres_req_up = 0;
572	}
573	else {
574	}
575	if (main_dbl_req_up == 1) {
576	if (main_dbl_val != main_dbl_val_t) {
577	main_dbl_val = main_dbl_val_t;
578	main_dbl_ev = 0;
579	}
580	else {
581	}
582	main_dbl_req_up = 0;
583	}
584	else {
585	}
586	if (main_zero_req_up == 1) {
587	if (main_zero_val != main_zero_val_t) {
588	main_zero_val = main_zero_val_t;
589	main_zero_ev = 0;
590	}
591	else {
592	}
593	main_zero_req_up = 0;
594	}
595	else {
596	}
597	if (main_clk_req_up == 1) {
598	if (main_clk_val != main_clk_val_t) {
599	main_clk_val = main_clk_val_t;
600	main_clk_ev = 0;
601	if (main_clk_val == 1) {
602	main_clk_pos_edge = 0;
603	main_clk_neg_edge = 2;
604	}
605	else {
606	main_clk_neg_edge = 0;
607	main_clk_pos_edge = 2;
608	}
609	}
610	else {
611	}
612	main_clk_req_up = 0;
613	}
614	else {
615	}
616	kernel_st = 3;
617	if (main_in1_ev == 0) {
618	main_in1_ev = 1;
619	}
620	else {
621	}
622	if (main_in2_ev == 0) {
623	main_in2_ev = 1;
624	}
625	else {
626	}
627	if (main_sum_ev == 0) {
628	main_sum_ev = 1;
629	}
630	else {
631	}
632	if (main_diff_ev == 0) {
633	main_diff_ev = 1;
634	}
635	else {
636	}
637	if (main_pres_ev == 0) {
638	main_pres_ev = 1;
639	}
640	else {
641	}
642	if (main_dbl_ev == 0) {
643	main_dbl_ev = 1;
644	}
645	else {
646	}
647	if (main_zero_ev == 0) {
648	main_zero_ev = 1;
649	}
650	else {
651	}
652	if (main_clk_ev == 0) {
653	main_clk_ev = 1;
654	}
655	else {
656	}
657	if (main_clk_pos_edge == 0) {
658	main_clk_pos_edge = 1;
659	}
660	else {
661	}
662	if (main_clk_neg_edge == 0) {
663	main_clk_neg_edge = 1;
664	}
665	else {
666	}
667	if (main_clk_pos_edge == 1) {
668	N_generate_st = 0;
669	}
670	else {
671	}
672	if (main_clk_pos_edge == 1) {
673	S1_addsub_st = 0;
674	}
675	else {
676	}
677	if (main_clk_pos_edge == 1) {
678	S2_presdbl_st = 0;
679	}
680	else {
681	}
682	if (main_clk_pos_edge == 1) {
683	S3_zero_st = 0;
684	}
685	else {
686	}
687	if (main_clk_pos_edge == 1) {
688	D_print_st = 0;
689	}
690	else {
691	}
692	if (main_in1_ev == 1) {
693	main_in1_ev = 2;
694	}
695	else {
696	}
697	if (main_in2_ev == 1) {
698	main_in2_ev = 2;
699	}
700	else {
701	}
702	if (main_sum_ev == 1) {
703	main_sum_ev = 2;
704	}
705	else {
706	}
707	if (main_diff_ev == 1) {
708	main_diff_ev = 2;
709	}
710	else {
711	}
712	if (main_pres_ev == 1) {
713	main_pres_ev = 2;
714	}
715	else {
716	}
717	if (main_dbl_ev == 1) {
718	main_dbl_ev = 2;
719	}
720	else {
721	}
722	if (main_zero_ev == 1) {
723	main_zero_ev = 2;
724	}
725	else {
726	}
727	if (main_clk_ev == 1) {
728	main_clk_ev = 2;
729	}
730	else {
731	}
732	if (main_clk_pos_edge == 1) {
733	main_clk_pos_edge = 2;
734	}
735	else {
736	}
737	if (main_clk_neg_edge == 1) {
738	main_clk_neg_edge = 2;
739	}
740	else {
741	}
742	if (N_generate_st == 0) {
743	}
744	else {
745	if (S1_addsub_st == 0) {
746	}
747	else {
748	if (S2_presdbl_st == 0) {
749	}
750	else {
751	if (S3_zero_st == 0) {
752	}
753	else {
754	if (D_print_st == 0) {
755	}
756	else {
757	goto while_1_break;
758	}
759	}
760	}
761	}
762	}
763	}
764	}
765	while_1_break: ;
766	}
767	return;
768	}
769	}
770
771	void main () {
772	//
773	// Number of lvals: 62
774	// Frama_C_interval: int (int min, int max)
775	// int (int min, int max)
776	// error: void (void)
777	// void (void)
778	// count: int
779	// int
780	// res: int
781	// int
782	// main_in1_val: int
783	// int
784	// main_in1_val_t: int
785	// int
786	// main_in1_ev: int
787	// int
788	// main_in1_req_up: int
789	// int
790	// main_in2_val: int
791	// int
792	// main_in2_val_t: int
793	// int
794	// main_in2_ev: int
795	// int
796	// main_in2_req_up: int
797	// int
798	// main_diff_val: int
799	// int
800	// main_diff_val_t: int
801	// int
802	// main_diff_ev: int
803	// int
804	// main_diff_req_up: int
805	// int
806	// main_sum_val: int
807	// int
808	// main_sum_val_t: int
809	// int
810	// main_sum_ev: int
811	// int
812	// main_sum_req_up: int
813	// int
814	// main_pres_val: int
815	// int
816	// main_pres_val_t: int
817	// int
818	// main_pres_ev: int
819	// int
820	// main_pres_req_up: int
821	// int
822	// main_dbl_val: int
823	// int
824	// main_dbl_val_t: int
825	// int
826	// main_dbl_ev: int
827	// int
828	// main_dbl_req_up: int
829	// int
830	// main_zero_val: int
831	// int
832	// main_zero_val_t: int
833	// int
834	// main_zero_ev: int
835	// int
836	// main_zero_req_up: int
837	// int
838	// main_clk_val: int
839	// int
840	// main_clk_val_t: int
841	// int
842	// main_clk_ev: int
843	// int
844	// main_clk_req_up: int
845	// int
846	// main_clk_pos_edge: int
847	// int
848	// main_clk_neg_edge: int
849	// int
850	// N_generate_st: int
851	// int
852	// N_generate_i: int
853	// int
854	// S1_addsub_st: int
855	// int
856	// S1_addsub_i: int
857	// int
858	// S2_presdbl_st: int
859	// int
860	// S2_presdbl_i: int
861	// int
862	// S3_zero_st: int
863	// int
864	// S3_zero_i: int
865	// int
866	// D_z: int
867	// int
868	// D_print_st: int
869	// int
870	// D_print_i: int
871	// int
872	// N_generate: void (void)
873	// void (void)
874	// S1_addsub: void (void)
875	// void (void)
876	// S2_presdbl: void (void)
877	// void (void)
878	// S3_zero: void (void)
879	// void (void)
880	// D_print: void (void)
881	// void (void)
882	// eval: void (void)
883	// void (void)
884	// start_simulation: void (void)
885	// void (void)
886	// n1: int
887	// int
888	// n2: int
889	// int
890	// n3: int
891	// int
892	// bound: int
893	// int
894	// i: int
895	// int
896	// flag: int
897	// int
898	//
899
900	D_print_i = __VERIFIER_nondet_int();
901	D_print_st = __VERIFIER_nondet_int();
902	D_z = __VERIFIER_nondet_int();
903	N_generate_i = __VERIFIER_nondet_int();
904	N_generate_st = __VERIFIER_nondet_int();
905	S1_addsub_i = __VERIFIER_nondet_int();
906	S1_addsub_st = __VERIFIER_nondet_int();
907	S2_presdbl_i = __VERIFIER_nondet_int();
908	S2_presdbl_st = __VERIFIER_nondet_int();
909	S3_zero_i = __VERIFIER_nondet_int();
910	S3_zero_st = __VERIFIER_nondet_int();
911	count = __VERIFIER_nondet_int();
912	main_clk_ev = __VERIFIER_nondet_int();
913	main_clk_neg_edge = __VERIFIER_nondet_int();
914	main_clk_pos_edge = __VERIFIER_nondet_int();
915	main_clk_req_up = __VERIFIER_nondet_int();
916	main_clk_val = __VERIFIER_nondet_int();
917	main_clk_val_t = __VERIFIER_nondet_int();
918	main_dbl_ev = __VERIFIER_nondet_int();
919	main_dbl_req_up = __VERIFIER_nondet_int();
920	main_dbl_val = __VERIFIER_nondet_int();
921	main_dbl_val_t = __VERIFIER_nondet_int();
922	main_diff_ev = __VERIFIER_nondet_int();
923	main_diff_req_up = __VERIFIER_nondet_int();
924	main_diff_val = __VERIFIER_nondet_int();
925	main_diff_val_t = __VERIFIER_nondet_int();
926	main_in1_ev = __VERIFIER_nondet_int();
927	main_in1_req_up = __VERIFIER_nondet_int();
928	main_in1_val = __VERIFIER_nondet_int();
929	main_in1_val_t = __VERIFIER_nondet_int();
930	main_in2_ev = __VERIFIER_nondet_int();
931	main_in2_req_up = __VERIFIER_nondet_int();
932	main_in2_val = __VERIFIER_nondet_int();
933	main_in2_val_t = __VERIFIER_nondet_int();
934	main_pres_ev = __VERIFIER_nondet_int();
935	main_pres_req_up = __VERIFIER_nondet_int();
936	main_pres_val = __VERIFIER_nondet_int();
937	main_pres_val_t = __VERIFIER_nondet_int();
938	main_sum_ev = __VERIFIER_nondet_int();
939	main_sum_req_up = __VERIFIER_nondet_int();
940	main_sum_val = __VERIFIER_nondet_int();
941	main_sum_val_t = __VERIFIER_nondet_int();
942	main_zero_ev = __VERIFIER_nondet_int();
943	main_zero_req_up = __VERIFIER_nondet_int();
944	main_zero_val = __VERIFIER_nondet_int();
945	main_zero_val_t = __VERIFIER_nondet_int();
946	res = __VERIFIER_nondet_int();
947
948
949
950	{
951	int n1 = 3;
952	int n2 = 5;
953	int n3 = 7;
954	res = 0;
955	auto int bound;
956	bound = __VERIFIER_nondet_int();
957	__VERIFIER_assume(bound >= 1);
958	{
959	{
960	count = 0;
961	main_in1_ev = 2;
962	main_in1_req_up = 0;
963	main_in2_ev = 2;
964	main_in2_req_up = 0;
965	main_diff_ev = 2;
966	main_diff_req_up = 0;
967	main_sum_ev = 2;
968	main_sum_req_up = 0;
969	main_pres_ev = 2;
970	main_pres_req_up = 0;
971	main_dbl_ev = 2;
972	main_dbl_req_up = 0;
973	main_zero_ev = 2;
974	main_zero_req_up = 0;
975	main_clk_val = 0;
976	main_clk_ev = 2;
977	main_clk_req_up = 0;
978	main_clk_pos_edge = 2;
979	main_clk_neg_edge = 2;
980	count = 0;
981	N_generate_i = 0;
982	S1_addsub_i = 0;
983	S2_presdbl_i = 0;
984	S3_zero_i = 0;
985	D_print_i = 0;
986	start_simulation();
987	}
988	{
989	int i = 0;
990	while (1) {
991	if (i < bound) {
992	}
993	else {
994	break;
995	}
996	{
997	if (i % n1 == 0) {
998	if (i % n2 == 0) {
999	if (i % n3 == 0) {
1000	res = i;
1001	}
1002	else {
1003	}
1004	}
1005	else {
1006	}
1007	}
1008	else {
1009	}
1010	i ++;
1011	int flag = res;
1012	while_2_continue: ;
1013	{
1014	main_clk_val_t = 1;
1015	main_clk_req_up = 1;
1016	start_simulation();
1017	count ++;
1018	}
1019
1020	if (res % 105 == 0) {
1021	;
1022	} else {
1023	error();
1024	}
1025
1026	if (count == 5) {
1027	if (! (D_z == 0)) {
1028	error();
1029	}
1030	else {
1031	}
1032	count = 0;
1033	}
1034	else {
1035	}
1036	{
1037	main_clk_val_t = 0;
1038	main_clk_req_up = 1;
1039	start_simulation();
1040
1041	}
1042	}
1043	}
1044	}
1045	}
1046	return;
1047	}}